$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $x$:ecl(${\it ds}$;${\it da}$). ($\uparrow$eclthrow?($x$)) $\Rightarrow$ (eclthrow{-}n($x$) $\in$ $\mathbb{N}$)